• Conference Object  

      An abstract channel specification and an algorithm implementing it using Java sockets 

      Georgiou, Chryssis; Shvartsman, A. A.; Musiał, Peter M.; Sonderegger, E. L. (2008)
      Models and specifications can be used in the design of distributed applications to formally reason about their safety properties. However, the benefits of using formal methods are often negated by the ad hoc process of ...
    • Article  

      Automated implementation of complex distributed algorithms specified in the IOA language 

      Georgiou, Chryssis; Lynch, N.; Mavrommatis, Panayiotis; Tauber, J. A. (2009)
      IOA is a formal language for describing Input/Output automata that serves both as a formal specification language and as a programming language (Garland et al. in http://theory.lcs.mit.edu/tds/ioa/manual.ps, 2004). The IOA ...
    • Conference Object  

      Brief announcement: A formal treatment of an abstract channel implementation using java sockets and TCP 

      Georgiou, Chryssis; Musiał, Peter M.; Shvartsman, A. A.; Sonderegger, E. L. (2007)
      Abstract models and specifications can be used in the design of distributed applications to formally reason about their safety properties. However, the benefits of using formal methods are offset by the challenging process ...
    • Article  

      Coverage analysis of mobile agent trajectory via state-based opacity formulations 

      Saboori, A.; Hadjicostis, Christoforos N. (2011)
      This paper performs coverage analysis of mobile agent trajectory utilizing discrete event system models and employing state-based notions of opacity. Non-deterministic finite automata with partial observation on their ...
    • Article  

      Fault-tolerant computation in groups and semigroups: Applications to automata, dynamic systems and Petri nets 

      Hadjicostis, Christoforos N.; Verghese, G. C. (2002)
      The traditional approach to fault-tolerant computation has been via modular hardware redundancy. Although universal and simple, modular redundancy is inherently expensive and inefficient. By exploiting particular structural ...
    • Conference Object  

      Intersection based decentralized diagnosis: Implementation and verification 

      Panteli, M.; Hadjicostis, Christoforos N. (Institute of Electrical and Electronics Engineers Inc., 2013)
      We consider decentralized diagnosis in discrete event systems that are modeled as non-deterministic finite automata and are observed, through distinct natural projection maps, at multiple observation sites. Specifically, ...
    • Article  

      On confluence in the π-caleulus 

      Philippou, Anna; Walker, D. (1997)
      An account of the basic theory of confluence in the 7r-calculus is presented, techniques for showing confluence of mobile systems are given, and the utility of some of the theory presented is illustrated via an analysis ...
    • Article  

      On the efficient use of multiple channels by single-receiver clients in wireless data broadcasting 

      Nicopolitidis, P.; Chrysostomou, Chrysostomos; Papadimitriou, Georgios I.; Pitsillides, Andreas; Pomportsis, A. S. (2014)
      This letter proposes an adaptive wireless push system for wireless data broadcasting environments, where multiple channels are available for broadcasting data from a broadcast server to a large number of mobile clients. ...
    • Article  

      The structure and complexity of Nash equilibria for a selfish routing game 

      Fotakis, Dimitris A.; Kontogiannis, Spyros C.; Koutsoupias, Elias; Mavronicolas, Marios; Spirakis, Paul G. (2002)
      In this work, we study the combinatorial structure and the computational complexity of Nash equilibria for a certain game that models selfish routing over a network consisting of m parallel links. We assume a collection ...
    • Conference Object  

      Synchronization-based fault detection in discrete event systems 

      Athanasopoulou, E.; Hadjicostis, Christoforos N. (2004)
      In this paper we study fault detection in systems that can be modeled as finite state machines (FSMs). We aim at detecting faults that manifest themselves as permanent changes in the next-state transition functionality of ...
    • Conference Object  

      Tempo-toolkit: Tempo to java translation module 

      Georgiou, Chryssis; Musiał, Peter M.; Ploutarchou, Christos (2013)
      TIOA is a formal language for modeling distributed, concurrent, and timed/untimed systems as collections of interacting state machines, called Timed Input/Output Automata. TIOA provide natural mathematical notations for ...
    • Conference Object  

      A trellis notion for distributed system diagnosis with sequential semantics 

      Fabre, E.; Hadjicostis, Christoforos N. (2006)
      We consider modular automata, obtained as a product of elementary components, and adopt the usual sequential semantics: runs of these systems are sequences of events (in contrast to partial orders). The set of all runs of ...
    • Article  

      Verification of initial-state opacity in security applications of discrete event systems 

      Saboori, A.; Hadjicostis, Christoforos N. (2013)
      In this paper, we formulate and analyze methodologies for verifying the notion of initial-state opacity in discrete event systems that are modeled as non-deterministic finite automata with partial observation on their ...